First UIP cut
なんで First なんだよtosuke.icon
conflict side からカットを動かしていったとき，最初に最新のレベルの変数が1つ(=unique!)になる点だからかも
UIP たちはグラフの部分集合としてリストを作るので，その先頭という意味だろうか
なんでこれがよさそうなの(私見)
最後に追加した decision point (=Last UIP)のレベルを n とすると，n-1 までの Implication Graph を decision side に含んでいい ある程度連結しているし，ここからも辺が伸びていくので，ここから頂点を外すのは分が悪い
なので，この Implication Graph と decision point を合わせた集合を decision side として，ここに頂点を付け足して良さそうなカットを探すのが丸そうということになる ここで，今見ている UIP から出る辺が1本だけある(=次の UIP がある)状態のとき，次の UIP を decision side としても生成される学習節は今の状態より長くならない
他の頂点からの合流があることによって短くなる可能性はある，つまり UIP を辿っている間は学習節の長さが単調減少する
実装としても候補を列挙して分岐を見つけたらその先を捨てるだけ(たぶん)なので，そこまで重くない。結果として損をすることはほぼなく得をする可能性があるということになる
思ったより保守的な戦略だった